/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;

import simhya.modelchecking.Formula;
import simhya.model.store.Store;
import simhya.matheval.SymbolArray;
import java.util.HashMap;
import java.util.ArrayList;
import simhya.dataprocessing.Trajectory;
import simhya.modelchecking.*;


/**
 *
 * @author Luca
 */
public class MTLformula implements Formula {
    MTLnode root;
    Threshold threshold;
    ArrayList<MTLatom> atomicNodes;
    Store store;



    private boolean varyInterval;
    private boolean varyRightBound;
    private int points;
    private int storeVars;
    private SMCtestData tester = null;
    private SMCestimateTrajectory estimator = null;
    private SMCcontroller controller = null;
    private boolean estimate;
    private boolean ready = false;


    public MTLformula(MTLnode root) {
        this.root = root;
        this.threshold = null;
        atomicNodes = new ArrayList<MTLatom>();
        root.collectAtomicNodes(atomicNodes);
        estimate = true;
        root.setTopNodeInfo();
    }

    public MTLformula(Threshold threshold, MTLnode root) {
        this.threshold = threshold;
        this.root = root;
        atomicNodes = new ArrayList<MTLatom>();
        root.collectAtomicNodes(atomicNodes);
        estimate = false;
        root.setTopNodeInfo();
    }

    public void initalize(Store store, SymbolArray localSymbols, HashMap predicatesToExpression) {
        this.store = store;
        this.storeVars  = store.getNumberOfVariables();
        root.initalize(store,localSymbols,predicatesToExpression);
        root.recomputeBounds(localSymbols);
    }

    public void recomputeBounds(SymbolArray localSymbols) {
        root.recomputeBounds(localSymbols);
        String s = threshold.getThresholdParameter();
        if (s != null) {
            int id = localSymbols.getSymbolId(s);
            double x = localSymbols.getValue(id);
            threshold.setThresholdValue(x);
        }
    }

    public String toFormulaTree() {
        String s = "";
        s += "Probability " + (threshold == null ? "=?" : threshold.toString()) + "\n";
        s += root.toFormulaTree(1);
        return s;
    }

    
    
    /**
     * This initializes the formula for estimation.
     * @param estimator
     * @param parameter
     * @param varyInterval
     * @param varyRightBound
     * @param points 
     */
    public void initializeForModelChecking(SMCestimateTrajectory estimator, String parameter, 
            boolean varyInterval, boolean varyRightBound, int points) {
        if (!this.estimate)
            throw new RuntimeException("This formula doea not support estimation, initialize it for testing");
        this.varyInterval = varyInterval;
        this.varyRightBound = varyRightBound;
        this.points = points;
        this.root.testAndSetExplorableTopNodes(parameter);
        this.estimator = estimator;
        this.controller = estimator;
        this.ready = true;
    }
    
    /**
     * This initializes the formula for model checking with testing.
     */
    public void initializeForModelChecking(SMCtestData tester) {
        if (this.estimate)
            throw new RuntimeException("This formula doea not support testing, initialize it for estimation");
        this.tester = tester;
        this.controller = tester;
        this.varyInterval = false;
        this.varyRightBound = true;
        this.points = 1;
        this.ready = true;
    }

    
    /**
     * this is the key method to call in a routine to model check a formula.
     * A simulator has to be used to feed trajectories to the method, one by one. 
     * Then each trajectory is model checked and the proper action is performed in 
     * terms of estimate or testing.
     * The method returns true if and ony if the model checking procedure has reached
     * an end, according to current accuracy criteria.
     * @param traj
     * @return 
     */
    public boolean modelCheckNextTrajectory(Trajectory traj) {
        //formula is not ready to be model checked. 
        if (!ready)
            //return true;
            throw new RuntimeException("Formula not ready to be model checked. Either model checking "
                    + "has not been initialized or it terminated already");
        //we init nodes
        this.root.initForModelChecking(points, traj.getPoints());
        //we compute truth value of atomic formulae
        this.setAtomicTruthValue(traj);
        double [] deltaTimes = computeTimeIncrements(traj);
        boolean [] truth = root.modelCheck(deltaTimes, varyInterval, varyRightBound, points);
        controller.addPoint(truth);
        boolean answer = controller.stop();
        if (answer) {
            ready = false;
            controller.finalize();
        }
        return answer;
    }
    
    
    /**
     * Computes the time increments for each state of the trajectory
     * @param traj
     * @return 
     */
    private double [] computeTimeIncrements(Trajectory traj) {
        int n = traj.getPoints();
        double [] dt = new double[n];
        dt[n-1] = 0;
        for (int i=0;i<n-1;i++)
            dt[i] = traj.getData(0, i+1) - traj.getData(0, i);
        return dt;
    }
    
    
    

    void setAtomicTruthValue(Trajectory traj) {
        double[] v = new double[this.storeVars];
        for (int i=0;i<traj.getPoints();i++) {
            //store variables are stored in position 1 to storeVars
            for (int j=1;j<=storeVars;j++)
                v[j] = traj.getData(i, j);
            store.setAllVariableValues(v);
            for (MTLatom n : this.atomicNodes)
                n.computeTruthValue(i);
        }
    }

    
    public boolean performsEstimate() {
        return this.estimate;
    }
    
    /**
     * Signals the abnormal termination of the model checking procedure. 
     */
    public void terminateModelChecking() {
        controller.finalize();
        this.ready = false;
    }
    
    
    public SMCoutput getSMCoutput() {
        if (ready)
            throw new RuntimeException("The model checking is not completed");
        if (estimate)
            if (this.estimator == null)
                throw new RuntimeException("Output is not present, I'm puzzled, sorry!");
            else return estimator;
        else
            if (this.tester == null)
                throw new RuntimeException("Output is not present, I'm puzzled, sorry!");
            else return tester;
    }

    /*
     * Notacce: devo gestire il setup del metodo e il setuo della struttura dati di output
     * devo mettere in piedi agoritmo, in cui faccio un while la struttura dati di output 
     * non mi dice stop o non raggiugno un upper bound?
     * La strttura dati di putput mi viene passata da fuori.
     *
     *
     *
     */

}
